Nuprl Lemma : p-mu-decider
11,40
postcript
pdf
A
:Type,
P
:(
A
). (
x
:
A
. Dec(
n
:
. (
(
P
(
x
,
n
)))))
(
x
:
A
.
y
:
+ Top. p-mu(
P
(
x
);
y
))
latex
ProofTree
Definitions
x
:
A
.
B
(
x
)
,
,
b
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Dec(
P
)
,
t
T
,
f
(
a
)
,
P
Q
,
Top
,
left
+
right
,
p-mu(
P
;
x
)
,
x
:
A
B
(
x
)
,
,
Type
Lemmas
p-mu-exists
origin
A:Type, P:(A
). (x:A. Dec(
n:. (
(P(x,n))))) 
(x:A. y: + Top. p-mu(P(x);y))
A:Type, P:(A). (x:A. Dec(n:. ((P(x,n))))) (x:A. y: + Top. p-mu(P(x);y))
x:A. B(x)b
B(x)x:A. B(x)
T QB(x)